Step of Proof: outr_wf 12,41

Inference at * 1 
Iof proof for Lemma outr wf:



1. A : Type
2. B : Type
3. x : A + B
4. (isl(x))
  outr(x B 
latex

 by ((D 3) 
CollapseTHENM (Reduce (-1))) 
latex


C1

C1: 3. x1 : A
C1: 4. False
C1:   outr(inl x1 )  B
C2

C2: 3. y : B
C2: 4. True
C2:   outr(inr y )  B
C.


Definitionsif b then t else f fi , ff, tt, isl(x), b, b

origin